| 1: | a__and(true,X) | → mark(X) | |
| 2: | a__and(false,Y) | → false | |
| 3: | a__if(true,X,Y) | → mark(X) | |
| 4: | a__if(false,X,Y) | → mark(Y) | |
| 5: | a__add(0,X) | → mark(X) | |
| 6: | a__add(s(X),Y) | → s(add(X,Y)) | |
| 7: | a__first(0,X) | → nil | |
| 8: | a__first(s(X),cons(Y,Z)) | → cons(Y,first(X,Z)) | |
| 9: | a__from(X) | → cons(X,from(s(X))) | |
| 10: | mark(and(X1,X2)) | → a__and(mark(X1),X2) | |
| 11: | mark(if(X1,X2,X3)) | → a__if(mark(X1),X2,X3) | |
| 12: | mark(add(X1,X2)) | → a__add(mark(X1),X2) | |
| 13: | mark(first(X1,X2)) | → a__first(mark(X1),mark(X2)) | |
| 14: | mark(from(X)) | → a__from(X) | |
| 15: | mark(true) | → true | |
| 16: | mark(false) | → false | |
| 17: | mark(0) | → 0 | |
| 18: | mark(s(X)) | → s(X) | |
| 19: | mark(nil) | → nil | |
| 20: | mark(cons(X1,X2)) | → cons(X1,X2) | |
| 21: | a__and(X1,X2) | → and(X1,X2) | |
| 22: | a__if(X1,X2,X3) | → if(X1,X2,X3) | |
| 23: | a__add(X1,X2) | → add(X1,X2) | |
| 24: | a__first(X1,X2) | → first(X1,X2) | |
| 25: | a__from(X) | → from(X) | |
| 26: | A__AND(true,X) | → MARK(X) | |
| 27: | A__IF(true,X,Y) | → MARK(X) | |
| 28: | A__IF(false,X,Y) | → MARK(Y) | |
| 29: | A__ADD(0,X) | → MARK(X) | |
| 30: | MARK(and(X1,X2)) | → A__AND(mark(X1),X2) | |
| 31: | MARK(and(X1,X2)) | → MARK(X1) | |
| 32: | MARK(if(X1,X2,X3)) | → A__IF(mark(X1),X2,X3) | |
| 33: | MARK(if(X1,X2,X3)) | → MARK(X1) | |
| 34: | MARK(add(X1,X2)) | → A__ADD(mark(X1),X2) | |
| 35: | MARK(add(X1,X2)) | → MARK(X1) | |
| 36: | MARK(first(X1,X2)) | → A__FIRST(mark(X1),mark(X2)) | |
| 37: | MARK(first(X1,X2)) | → MARK(X1) | |
| 38: | MARK(first(X1,X2)) | → MARK(X2) | |
| 39: | MARK(from(X)) | → A__FROM(X) | |